%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% Basic Definitions and Macros 
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% Authors: Carlos Olarte, Catuscia Palamidessi and Frank D. Valencia
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%   Packages required  %%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{proof}
\usepackage{myproof}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%% Sections
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newtheorem{definition}{Definition} 
%\newtheorem{notation}{Notation} 
%\newtheorem{observation}{Observation} 
%\newtheorem{theorem}{Theorem} 
%\newtheorem{lemma}{Lemma}
%\newtheorem{corollary}{Corollary} 
%\newtheorem{example}{Example} 
%\newtheorem{remark}{Remark} 
%\newtheorem{proposition}{Proposition} 
 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%% Many-sorted Extension
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\degree}{degree}
\newcommand{\lift}[3]{#3\hspace{-0.13cm}\downarrow ^{#1}_{#2}}
\newcommand{\sorted}[2]{#2{_{\sigma \hspace{-0.052cm}_{#1}}}}
\newcommand{\sort}[1]{\sigma_{#1}}
\newcommand{\Lift}[2]{#2\hspace{-0.10cm}\Downarrow\hspace{-0.08cm}^{#1}}
\newcommand{\Liftterm}[2]{#2\hspace{-0.10cm}\Downarrow\hspace{-0.08cm}^{#1}_t}
\long\def\comment[#1]{}
\newcommand{\tab}{\ \ \ \  }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  (u)tcc Operators  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\fv}{{\it fv}}
\newcommand{\bv}{{\it bv}} 
\newcommand{\tellp}[1]{\mathbf{tell}(#1)}
\newcommand{\whenp}[2]{\mathbf{when} \  #1 \  \mathbf{do} \ #2}
\newcommand{\choicep}[3] {\sum_{#1}\whenp{#2}{#3}}
\newcommand{\wheneverp}[2]{\mathbf{whenever} \  #1 \  \mathbf{do} \ #2}
\newcommand{\absp}[3]{(\mathbf{abs} \  #1;#2) \, #3}
\newcommand{\absptrue}[2]{(\mathbf{abs} \  #1) \, #2}
\newcommand{\waitp}[3]{(\mathbf{wait} \  #1 ; #2) \  \mathbf{do} \ #3}
\newcommand{\repeatp}[1]{\mathbf{repeat} \ #1}
\newcommand{\nextp}[1]{\mathbf{next}\, #1}
\newcommand{\unlessp}[2]{\mathbf{unless} \  #1 \  \nextp{#2}}
\newcommand{\localp}[2]{(\mathbf{local} \, #1)  \, #2}
\newcommand{\parp}[2]{ #1 \, \parallel \, #2}
\newcommand{\bangp}[1]{ !\,#1}
\newcommand{\starp}[1]{ \star\,#1}
\newcommand{\skipp}{\mathbf{skip}}
\newcommand{\abortp}{\mathbf{abort}}
\newcommand{\waitpp}[3]{(\underline{\mathbf{wait}} \  #1 ; #2) \  \mathbf{do} \ #3}
\newcommand{\tellpp}[1]{\underline{\mathbf{tell}}(#1)}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  Internal and Observable rules
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\rTell}{\rm R_{T}}
\newcommand{\rPar}{\rm R_{P}}
\newcommand{\rParR}{\rm R_{PR}}
\newcommand{\rParL}{\rm R_{PL}}
\newcommand{\rBang}{\rm R_{R}}
\newcommand{\rAbs}{\rm R_{A}}
\newcommand{\rLocal}{\rm R_{L}}
\newcommand{\rStruct}{\rm R_{S}}
\newcommand{\rUnless}{\rm R_{U}}
\newcommand{\rObserv}{\rm R_{O}}
\newcommand{\rCall}{\rm R_{C}}
\newcommand{\rStar}{\rm R_{S}}
\newcommand{\rChoice}{\rm R_{SUM}}

%%%%%%
% RULES SECURITY CONS SYSTEM
%%%%%%
\newcommand{\rEnc}{\rm \scriptsize{ENC}} % Encrypting (forwarding)
\newcommand{\rDec}{\rm \scriptsize{DEC}} %Decrypting
\newcommand{\rPair}{\rm \scriptsize{PAIR}} %Pairing
\newcommand{\rPrj}{\rm \scriptsize{PRJ}} %Projection
%% Symbolic
\newcommand{\rAbsSym}{\rm R_{As}}
\newcommand{\rObservSym}{\rm R_{Os}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  Temporal Logic
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\nextt}{\mbox{$\circ$}}
\newcommand{\sometime}{\Diamond}
\newcommand{\always}{\square}
\newcommand{\past}[1]{\circleddash#1}

\DeclareMathOperator{\tand} {\dot\wedge }
\DeclareMathOperator{\tor}{\dot\vee }
\DeclareMathOperator{\timply}{\dot\Rightarrow }


\DeclareMathOperator{\tneg}{\dot\neg}
\DeclareMathOperator{\texists}{\dot\exists}
\DeclareMathOperator{\ttrue}{{\dot{\true}}}
\DeclareMathOperator{\tfalse}{{\dot{\false}}}
\newcommand{\modelsnltl}{\models_{\textup{CLTL}}}
\newcommand{\modelsltl}{\models_{\textup{\tiny{$\cM(\cL)$}}}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  Miscellaneous 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\defsymbol}{\stackrel{\textup{\texttt{def}}}  {=}} 
 \newcommand{\defp}[2]{#1 \defsymbol #2}

\newcommand{\ntcc}{\texttt{ntcc}\xspace}
\newcommand{\tcc}{\texttt{tcc}\xspace}
\newcommand{\utcc}{\texttt{utcc}\xspace}
\newcommand{\ccp}{CCP\xspace}
\newcommand{\rtcc}{\texttt{rtcc}\xspace}
\newcommand{\pntcc}{\texttt{pntcc}\xspace}

\newcommand{\exch}{\textup {\textrm exch}}
\newcommand{\Dom} {{\mathcal{D}}}
\newcommand{\maxv} {{\it max}}
\newcommand{\FD} {\mathbf{FD}}
\renewcommand{\iff}{\!\!\!\!\mbox{iff}\!\!\!\!\!}
\newcommand{\os}{[\![}
\newcommand{\cs}{]\!]}
\newcommand{\denot}[1]{\os #1 \cs}
\newcommand{\ldenot}[1]{\os #1 \cs_l}
\newcommand{\C}{\mathcal{C}}
\renewcommand{\sp}{\it sp}
\DeclareMathOperator{\sps}{\it sp_s}
\newcommand{\stf}{\it stf}
\newcommand{\Processes}{\it Proc}
\newcommand{\Processesr}{{\it Proc}^r}
\newcommand{\const}{\mathcal{C}}
\newcommand{\symconst}{\mathcal{C}_s}


\DeclareMathOperator{\outp}{\textup{\texttt{out}}}
\DeclareMathOperator{\noncep}{\textup{\texttt{nonce}}}
\DeclareMathOperator{\secretp}{\textup{\texttt{secret}}}
\DeclareMathOperator{\failp}{\textup{\texttt{fail}}}
\DeclareMathOperator{\encp}{\it{enc}}
\DeclareMathOperator{\pairp}{\it{pair}}
\DeclareMathOperator{\invp}{\it{inv}}
\DeclareMathOperator{\keypp}{\it{key_p}}
\DeclareMathOperator{\priv}{\it{priv}}
\DeclareMathOperator{\pub}{\it{pub}}


\newcommand{\tuplee}{\it Formulae}
\newcommand{\mconf}[1]{\left\langle {#1} \right\rangle}
\newcommand{\tuple}[2]{\left\langle {#1,#2} \right\rangle}
\newcommand{\lequiv}[1]{\sim_{#1}^{{\it o}}}
\newcommand{\lcong}[1]{\approx_{#1}^{{\it o}}}
\newcommand{\ioequiv}[1]{\sim_{#1}^{{\it io}}}
\newcommand{\oequiv}[1]{\sim_{#1}^{{\it o}}}
\newcommand{\spequiv}[1]{\sim_{#1}^{{\it sp}}}
\newcommand{\ioequivs}[1]{\sim_{s#1}^{{\it io}}}
\newcommand{\oequivs}[1]{\sim_{s#1}^{{\it o}}}
\newcommand{\spequivs}[1]{\sim_{s#1}^{{\it sp}}}

\newcommand{\iocong}[1]{\approx_{#1}^{{\it io}}}

\newcommand{\iobehav}[1]{{\it io}(#1)}
\newcommand{\obehav}[1]{{\it o}(#1)}
\newcommand{\iobehavs}[1]{{\it io_s}(#1)}
\newcommand{\obehavs}[1]{{\it o_s}(#1)}

\newcommand{\entails}{\vdash}
\newcommand{\basiccons}{{\it bcons}}

\newcommand{\cut}{\it cut}
%\newcommand{\terms}{\textup{\texttt{terms}}}
\newcommand{\entailsec}{\vdash_{\texttt{s}}}
\newcommand{\notentails}{\not \entails}

\newcommand{\obs}[1]
{\marginpar{\baselineskip0ex\rule{2,5cm}{0.5pt}\\[0ex]{\tiny\textsf{#1}}}}

\newcommand{\Obs}{\mathcal{O}}
\newcommand{\Obssym}{\mathcal{O}_s}

\newcommand*{\powerset}{\cP}

\long\def\comment#1{}

\newcommand{\geqsym}{\succeq}
\newcommand{\eqsym}{\approx}
\newcommand{\gsym}{\succ}


\newcommand{\TLVFV}{TLV-\textup{\texttt{flex}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  Reduction Arrows
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\redi}{\longrightarrow }
\newcommand{\redisym}{\longrightarrow_{s} }
\newcommand{\notredi}{ \not \hspace{-.1cm} \redi }
\newcommand{\rede}[1]{\stackrel{\,\,#1\,\,}{\,\,
=\hspace{-0.1cm}=\hspace{-0.1cm}=\hspace{-0.1cm}\Longrightarrow}} 
\newcommand{\redel}[1]{\stackrel{#1}{\,\,=\hspace{-0.1cm}\Longrightarrow}} 
\newcommand{\redeinf}[1]{\stackrel{\,\,#1\,\,}{\,\,
=\hspace{-0.1cm}=\hspace{-0.1cm}=\hspace{-0.1cm}\Longrightarrow}\!\!\!\
^\omega} 
\newcommand{\redelinf}[1]{\stackrel{#1}{\,\,=\hspace{-0.1cm}\Longrightarrow}\!\!\!\ ^\omega}
\newcommand{\dsem}[1]{[ \! [ \, {#1 } \, ] \!  ]} 
\newcommand{\outputp}[1]{\textup{\texttt{output}}(#1)}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  Logic Connectives 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\newcommand{\imply}{\Rightarrow}

\DeclareMathOperator{\true}{\textup{\texttt{true}}}

\DeclareMathOperator{\false}{\textup{\texttt{false}}}

\DeclareMathOperator{\modulo}{\, \textup{\texttt{mod}}\, }



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  Hyphenations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\hyphenation{un-boun-ded}
\hyphenation{research}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  Calligraphic 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\cA{\mathcal{A}}
\def\cC{\mathcal{C}}
\def\cD{\mathcal{D}}
\def\cE{\mathcal{E}}
\def\cF{\mathcal{F}}
\def\cG{\mathcal{G}}
\def\cH{\mathcal{H}}
\def\cI{\mathcal{I}}
\def\cK{\mathcal{K}}
\def\cL{\mathcal{L}}
\def\cM{\mathcal{M}}
\def\cN{\mathcal{N}}
\def\cV{\mathcal{V}}
\def\cO{\mathcal{O}}
\def\cP{\mathcal{P}}
\def\cR{\mathcal{R}}
\def\cS{\mathcal{S}}
\def\cT{\mathcal{T}}
\def\cX{\mathcal{X}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  Writing shortcuts.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand*{\ie}{i.e. } 
\newcommand*{\eg}{e.g. } 
\newcommand*{\st}{s.t} 
\newcommand*{\wrt}	{wrt}
\newcommand*{\csystem}	{cs}
\newcommand*{\io}{\it io}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  Colors
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\red}[1]{\textcolor{red}{#1} }
\newcommand{\blue}[1]{\textcolor{blue}{#1} }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%  Abstract Interpretation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\A{\mathbb{A}}
\def\E{\mathbb{E}}
\newcommand*{\CSymbols}{\cC}
\newcommand*{\PlainProc}[1]{\tilde{#1}}
\newcommand*{\FFFormula}{{\it F\!F}}
\newcommand*{\FFSequences}{\cF^\omega}
\newcommand*{\PastMonotonic}{ {\it P\!M}}
\newcommand*{\PastSeq}[1]{\overline{#1}}
\newcommand*{\FixFormula}{{\it Fix}}
\newcommand*{\FreeLocal}[2]{\mathsf{L} \os #1\cs_{#2}}
\newcommand*{\CutF}{{\it Cut_{\it F}}}
\newcommand*{\CutP}{{\it Cut_{\it P}}}
\newcommand*{\FutureFree}{{\it FF}}
\newcommand*{\Monotonic}{{\it {\bf Mon}}}

\newcommand*{\CTerms}{\cT(\CSymbols,\Variables)}
\newcommand*{\DSymbols}{\cD}
\newcommand*{\Fix}[2][]{\cF^{#1}_{#2}}
\newcommand*{\FixR}[2][]{{\ensuremath\widetilde{\cF}^{#1}_{#2}}}
\newcommand*{\GCTerms}{{\cT(\CSymbols)}}
\newcommand*{\GTerms}{{\cT(\Symbols)}}
\newcommand*{\I}[1][]	{{\mathcal{I}^{#1}}}
\newcommand*{\Nf}{\ensuremath{\mathop{\mathsf{nf}}}}
\newcommand*{\OTerms}{{\cT_{\Omega}(\Symbols,\Variables)}}
\newcommand*{\Pos}{{{\cal P}os}}
\newcommand*{\Sem}[2][]{\mathit{Sem}^{#1}_{#2}}
\newcommand*{\Symbols}{{\Sigma}}
\newcommand*{\TR}[2][]{T^{#1}_{#2}}
\newcommand*{\TRR}[2][]{{\ensuremath\widetilde{T}^{#1}_{#2}}}
\newcommand*{\Terms}{{\cT(\Symbols,\Variables)}}
\newcommand*{\Val}{{\ensuremath{\mathop{\mathsf{val}}}}}
\newcommand*{\Variables}{\cV}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MINSKY INSTRUCTIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\DeclareMathOperator{\haltp}{\textup{\texttt{halt}}}
\DeclareMathOperator{\nothaltp}{\textup{\texttt{running}}}
\DeclareMathOperator{\gotop}{\textup{\texttt{goto}}}
\DeclareMathOperator{\ifp}{\textup{\texttt{if}}}
\DeclareMathOperator{\elsep}{\textup{\texttt{else}}}
\DeclareMathOperator{\thenp}{\textup{\texttt{then}}}
\newcommand{\ifelsep}[3]{\ifp \ #1 \ \thenp \ #2 \ \elsep \ #3}
\newcommand{\outmin}[3]{\outp^{#1}_{#2}(#3)}
\newcommand{\encinstruction}{ins}


%%%%%%%%%%%%%%%%%%%%%%%%
% DENOTATIONAL SEMANTICS
%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand*{\csequences}{\cC^\omega}
\newcommand{\rdAbort}{\rm D_{Ab}}
\newcommand{\rdSkip}{\rm D_{S}}
\newcommand{\rdTell}{\rm D_{T}}
\newcommand{\rdNext}{\rm D_{N}}
\newcommand{\rdPar}{\rm D_{P}}
\newcommand{\rdBang}{\rm D_{R}}
\newcommand{\rdAbs}{\rm D_{A}}
\newcommand{\rdLocal}{\rm D_{L}}
\newcommand{\rdUnless}{\rm D_{U}}


%%%%%%%%%%%%%%%%%%%%%%
% COMMENTS
%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\comments}[1]{ }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% RECURSION
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\DeclareMathOperator{\callp}{\textup{\texttt{call}}}
\DeclareMathOperator{\repl}{\textup{\texttt{rep}}}
\DeclareMathOperator{\recl}{\textup{\texttt{rec}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MISC
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\afterp}[2]{#1 \ \textup{\texttt{after} } \ #2}
\newcommand{\lub}{\it lub}
\newcommand{\glb}{\it glb}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% THE SECURITY LANGUAGE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\nilP}{{\bf nil}}
\newcommand{\newP}[2]{{\bf new}(#1)#2}
\newcommand{\outP}[1]{{\bf out}(#1)}
\newcommand{\inP}[1]{{\bf in}\ #1}
\newcommand{\matchP}[2]{[#1].#2}
\newcommand{\parallelP}{\parallel}
\newcommand{\spitoutcc}{\it I}
\newcommand{\denotspi}[1]{\os #1 \cs_{\it SCCP}}
\newcommand{\LangSec}{SCCP}




